; COMMAND-LINE: --finite-model-find
(set-logic ALL)
(set-info :status unsat)
(declare-sort $$unsorted 0)
(declare-fun tptp.big_f ($$unsorted $$unsorted) Bool)
(declare-fun tptp.a () $$unsorted)
(assert (forall ((X $$unsorted) (Y $$unsorted)) (or (not (tptp.big_f X Y)) (= X tptp.a))))
(declare-fun tptp.b () $$unsorted)
(assert (forall ((X $$unsorted) (Y $$unsorted)) (or (not (tptp.big_f X Y)) (= Y tptp.b))))
(assert (forall ((X $$unsorted) (Y $$unsorted)) (or (not (= X tptp.a)) (not (= Y tptp.b)) (tptp.big_f X Y))))
(declare-fun tptp.f ($$unsorted) $$unsorted)
(declare-fun tptp.g ($$unsorted) $$unsorted)
(assert (forall ((Y $$unsorted) (X $$unsorted)) (let ((_let_1 (tptp.f X))) (or (not (tptp.big_f Y _let_1)) (not (= Y (tptp.g X))) (= _let_1 X)))))
(declare-fun tptp.h ($$unsorted $$unsorted) $$unsorted)
(assert (forall ((Y $$unsorted) (X $$unsorted) (Z $$unsorted)) (let ((_let_1 (tptp.f X))) (let ((_let_2 (tptp.big_f (tptp.h X Z) _let_1))) (or (not (tptp.big_f Y _let_1)) (= Y (tptp.g X)) _let_2 (not _let_2))))))
(assert (forall ((Y $$unsorted) (X $$unsorted)) (let ((_let_1 (tptp.f X))) (or (not (= Y (tptp.g X))) (tptp.big_f Y _let_1) (= _let_1 X)))))
(assert (forall ((Y $$unsorted) (X $$unsorted) (Z $$unsorted)) (let ((_let_1 (tptp.h X Z))) (let ((_let_2 (tptp.f X))) (or (not (= Y (tptp.g X))) (tptp.big_f Y _let_2) (tptp.big_f _let_1 _let_2) (= _let_1 Z))))))
(assert (forall ((Y $$unsorted) (X $$unsorted) (Z $$unsorted)) (let ((_let_1 (tptp.f X))) (let ((_let_2 (tptp.h X Z))) (or (not (= Y (tptp.g X))) (tptp.big_f Y _let_1) (not (= _let_2 Z)) (not (tptp.big_f _let_2 _let_1)))))))
(assert (forall ((X $$unsorted) (Z $$unsorted)) (let ((_let_1 (tptp.h X Z))) (let ((_let_2 (tptp.f X))) (or (not (= _let_2 X)) (tptp.big_f _let_1 _let_2) (= _let_1 Z))))))
(assert (forall ((X $$unsorted) (Z $$unsorted)) (let ((_let_1 (tptp.f X))) (let ((_let_2 (tptp.h X Z))) (or (not (= _let_1 X)) (not (= _let_2 Z)) (not (tptp.big_f _let_2 _let_1)))))))
(set-info :filename SYN075-1)
(check-sat)
